$\forall$$A$:MsgA, $x$:Id, $k$:Knd, $s_{1}$, $s_{2}$:$A$.state, $v$:$A$.da($k$).
\\[0ex]ma{-}frame{-}compat($A$;$A$)
\\[0ex]$\Rightarrow$ $\neg$$A$.rframe($k$ reads $x$)
\\[0ex]$\Rightarrow$ ($s_{1}$ $\equiv$ $s_{2}$ mod $x$)
\\[0ex]$\Rightarrow$ $A$.sends($k$,$s_{1}$,$v$) $=$ $A$.sends($k$,$s_{2}$,$v$) $\in$ $A$.Msg List